$\forall$${\it ds}$:fpf(Id; $x$.Type), $a$,$b$:fpf((:Knd $\times$ Id); ${\it kz}$.top).
\\[0ex]update{-}spec{-}decl($a$; ${\it ds}$)
\\[0ex]$\Rightarrow$ update{-}spec{-}decl($b$; ${\it ds}$)
\\[0ex]$\Rightarrow$ update{-}spec{-}decl(update{-}spec{-}join($a$; $b$); ${\it ds}$)